Left Termination of the query pattern myis_in_2(a, g) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

myis(Z, X) :- evaluate(X, Z).
evaluate(+(X, Y), Z) :- ','(evaluate(X, X1), ','(evaluate(Y, Y1), add(X1, Y1, Z))).
evaluate(-(X, Y), Z) :- ','(evaluate(X, X1), ','(evaluate(Y, Y1), sub(X1, Y1, Z))).
evaluate(*(X, Y), Z) :- ','(evaluate(X, X1), ','(evaluate(Y, Y1), mult(X1, Y1, Z))).
evaluate(X, X) :- myinteger(X).
myinteger(s(X)) :- myinteger(X).
myinteger(0).
add(s(X), Y, s(Z)) :- add(X, Y, Z).
add(0, X, X).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
mult(s(X), Y, R) :- ','(mult(X, Y, Z), add(Y, Z, R)).
mult(0, Y, 0).
notEq(s(X), s(Y)) :- notEq(X, Y).
notEq(s(X), 0).
notEq(0, s(X)).
lt(s(X), s(Y)) :- lt(X, Y).
lt(0, s(Y)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).

Queries:

myis(a,g).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

myis_in(Z, X) → U1(Z, X, evaluate_in(X, Z))
evaluate_in(X, X) → U11(X, myinteger_in(X))
myinteger_in(0) → myinteger_out(0)
myinteger_in(s(X)) → U12(X, myinteger_in(X))
U12(X, myinteger_out(X)) → myinteger_out(s(X))
U11(X, myinteger_out(X)) → evaluate_out(X, X)
evaluate_in(*(X, Y), Z) → U8(X, Y, Z, evaluate_in(X, X1))
evaluate_in(-(X, Y), Z) → U5(X, Y, Z, evaluate_in(X, X1))
evaluate_in(+(X, Y), Z) → U2(X, Y, Z, evaluate_in(X, X1))
U2(X, Y, Z, evaluate_out(X, X1)) → U3(X, Y, Z, X1, evaluate_in(Y, Y1))
U3(X, Y, Z, X1, evaluate_out(Y, Y1)) → U4(X, Y, Z, add_in(X1, Y1, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U4(X, Y, Z, add_out(X1, Y1, Z)) → evaluate_out(+(X, Y), Z)
U5(X, Y, Z, evaluate_out(X, X1)) → U6(X, Y, Z, X1, evaluate_in(Y, Y1))
U6(X, Y, Z, X1, evaluate_out(Y, Y1)) → U7(X, Y, Z, sub_in(X1, Y1, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U14(X, Y, Z, sub_in(X, Y, Z))
U14(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U7(X, Y, Z, sub_out(X1, Y1, Z)) → evaluate_out(-(X, Y), Z)
U8(X, Y, Z, evaluate_out(X, X1)) → U9(X, Y, Z, X1, evaluate_in(Y, Y1))
U9(X, Y, Z, X1, evaluate_out(Y, Y1)) → U10(X, Y, Z, mult_in(X1, Y1, Z))
mult_in(0, Y, 0) → mult_out(0, Y, 0)
mult_in(s(X), Y, R) → U15(X, Y, R, mult_in(X, Y, Z))
U15(X, Y, R, mult_out(X, Y, Z)) → U16(X, Y, R, add_in(Y, Z, R))
U16(X, Y, R, add_out(Y, Z, R)) → mult_out(s(X), Y, R)
U10(X, Y, Z, mult_out(X1, Y1, Z)) → evaluate_out(*(X, Y), Z)
U1(Z, X, evaluate_out(X, Z)) → myis_out(Z, X)

The argument filtering Pi contains the following mapping:
myis_in(x1, x2)  =  myis_in(x2)
U1(x1, x2, x3)  =  U1(x3)
evaluate_in(x1, x2)  =  evaluate_in(x1)
U11(x1, x2)  =  U11(x1, x2)
myinteger_in(x1)  =  myinteger_in(x1)
0  =  0
myinteger_out(x1)  =  myinteger_out
s(x1)  =  s(x1)
U12(x1, x2)  =  U12(x2)
evaluate_out(x1, x2)  =  evaluate_out(x2)
*(x1, x2)  =  *(x1, x2)
U8(x1, x2, x3, x4)  =  U8(x2, x4)
-(x1, x2)  =  -(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x4)
+(x1, x2)  =  +(x1, x2)
U2(x1, x2, x3, x4)  =  U2(x2, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x4, x5)
U4(x1, x2, x3, x4)  =  U4(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U13(x1, x2, x3, x4)  =  U13(x4)
U6(x1, x2, x3, x4, x5)  =  U6(x4, x5)
U7(x1, x2, x3, x4)  =  U7(x4)
sub_in(x1, x2, x3)  =  sub_in(x1, x2)
sub_out(x1, x2, x3)  =  sub_out(x3)
U14(x1, x2, x3, x4)  =  U14(x4)
U9(x1, x2, x3, x4, x5)  =  U9(x4, x5)
U10(x1, x2, x3, x4)  =  U10(x4)
mult_in(x1, x2, x3)  =  mult_in(x1, x2)
mult_out(x1, x2, x3)  =  mult_out(x3)
U15(x1, x2, x3, x4)  =  U15(x2, x4)
U16(x1, x2, x3, x4)  =  U16(x4)
myis_out(x1, x2)  =  myis_out(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

myis_in(Z, X) → U1(Z, X, evaluate_in(X, Z))
evaluate_in(X, X) → U11(X, myinteger_in(X))
myinteger_in(0) → myinteger_out(0)
myinteger_in(s(X)) → U12(X, myinteger_in(X))
U12(X, myinteger_out(X)) → myinteger_out(s(X))
U11(X, myinteger_out(X)) → evaluate_out(X, X)
evaluate_in(*(X, Y), Z) → U8(X, Y, Z, evaluate_in(X, X1))
evaluate_in(-(X, Y), Z) → U5(X, Y, Z, evaluate_in(X, X1))
evaluate_in(+(X, Y), Z) → U2(X, Y, Z, evaluate_in(X, X1))
U2(X, Y, Z, evaluate_out(X, X1)) → U3(X, Y, Z, X1, evaluate_in(Y, Y1))
U3(X, Y, Z, X1, evaluate_out(Y, Y1)) → U4(X, Y, Z, add_in(X1, Y1, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U4(X, Y, Z, add_out(X1, Y1, Z)) → evaluate_out(+(X, Y), Z)
U5(X, Y, Z, evaluate_out(X, X1)) → U6(X, Y, Z, X1, evaluate_in(Y, Y1))
U6(X, Y, Z, X1, evaluate_out(Y, Y1)) → U7(X, Y, Z, sub_in(X1, Y1, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U14(X, Y, Z, sub_in(X, Y, Z))
U14(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U7(X, Y, Z, sub_out(X1, Y1, Z)) → evaluate_out(-(X, Y), Z)
U8(X, Y, Z, evaluate_out(X, X1)) → U9(X, Y, Z, X1, evaluate_in(Y, Y1))
U9(X, Y, Z, X1, evaluate_out(Y, Y1)) → U10(X, Y, Z, mult_in(X1, Y1, Z))
mult_in(0, Y, 0) → mult_out(0, Y, 0)
mult_in(s(X), Y, R) → U15(X, Y, R, mult_in(X, Y, Z))
U15(X, Y, R, mult_out(X, Y, Z)) → U16(X, Y, R, add_in(Y, Z, R))
U16(X, Y, R, add_out(Y, Z, R)) → mult_out(s(X), Y, R)
U10(X, Y, Z, mult_out(X1, Y1, Z)) → evaluate_out(*(X, Y), Z)
U1(Z, X, evaluate_out(X, Z)) → myis_out(Z, X)

The argument filtering Pi contains the following mapping:
myis_in(x1, x2)  =  myis_in(x2)
U1(x1, x2, x3)  =  U1(x3)
evaluate_in(x1, x2)  =  evaluate_in(x1)
U11(x1, x2)  =  U11(x1, x2)
myinteger_in(x1)  =  myinteger_in(x1)
0  =  0
myinteger_out(x1)  =  myinteger_out
s(x1)  =  s(x1)
U12(x1, x2)  =  U12(x2)
evaluate_out(x1, x2)  =  evaluate_out(x2)
*(x1, x2)  =  *(x1, x2)
U8(x1, x2, x3, x4)  =  U8(x2, x4)
-(x1, x2)  =  -(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x4)
+(x1, x2)  =  +(x1, x2)
U2(x1, x2, x3, x4)  =  U2(x2, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x4, x5)
U4(x1, x2, x3, x4)  =  U4(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U13(x1, x2, x3, x4)  =  U13(x4)
U6(x1, x2, x3, x4, x5)  =  U6(x4, x5)
U7(x1, x2, x3, x4)  =  U7(x4)
sub_in(x1, x2, x3)  =  sub_in(x1, x2)
sub_out(x1, x2, x3)  =  sub_out(x3)
U14(x1, x2, x3, x4)  =  U14(x4)
U9(x1, x2, x3, x4, x5)  =  U9(x4, x5)
U10(x1, x2, x3, x4)  =  U10(x4)
mult_in(x1, x2, x3)  =  mult_in(x1, x2)
mult_out(x1, x2, x3)  =  mult_out(x3)
U15(x1, x2, x3, x4)  =  U15(x2, x4)
U16(x1, x2, x3, x4)  =  U16(x4)
myis_out(x1, x2)  =  myis_out(x1)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

MYIS_IN(Z, X) → U11(Z, X, evaluate_in(X, Z))
MYIS_IN(Z, X) → EVALUATE_IN(X, Z)
EVALUATE_IN(X, X) → U111(X, myinteger_in(X))
EVALUATE_IN(X, X) → MYINTEGER_IN(X)
MYINTEGER_IN(s(X)) → U121(X, myinteger_in(X))
MYINTEGER_IN(s(X)) → MYINTEGER_IN(X)
EVALUATE_IN(*(X, Y), Z) → U81(X, Y, Z, evaluate_in(X, X1))
EVALUATE_IN(*(X, Y), Z) → EVALUATE_IN(X, X1)
EVALUATE_IN(-(X, Y), Z) → U51(X, Y, Z, evaluate_in(X, X1))
EVALUATE_IN(-(X, Y), Z) → EVALUATE_IN(X, X1)
EVALUATE_IN(+(X, Y), Z) → U21(X, Y, Z, evaluate_in(X, X1))
EVALUATE_IN(+(X, Y), Z) → EVALUATE_IN(X, X1)
U21(X, Y, Z, evaluate_out(X, X1)) → U31(X, Y, Z, X1, evaluate_in(Y, Y1))
U21(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
U31(X, Y, Z, X1, evaluate_out(Y, Y1)) → U41(X, Y, Z, add_in(X1, Y1, Z))
U31(X, Y, Z, X1, evaluate_out(Y, Y1)) → ADD_IN(X1, Y1, Z)
ADD_IN(s(X), Y, s(Z)) → U131(X, Y, Z, add_in(X, Y, Z))
ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)
U51(X, Y, Z, evaluate_out(X, X1)) → U61(X, Y, Z, X1, evaluate_in(Y, Y1))
U51(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
U61(X, Y, Z, X1, evaluate_out(Y, Y1)) → U71(X, Y, Z, sub_in(X1, Y1, Z))
U61(X, Y, Z, X1, evaluate_out(Y, Y1)) → SUB_IN(X1, Y1, Z)
SUB_IN(s(X), s(Y), Z) → U141(X, Y, Z, sub_in(X, Y, Z))
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
U81(X, Y, Z, evaluate_out(X, X1)) → U91(X, Y, Z, X1, evaluate_in(Y, Y1))
U81(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
U91(X, Y, Z, X1, evaluate_out(Y, Y1)) → U101(X, Y, Z, mult_in(X1, Y1, Z))
U91(X, Y, Z, X1, evaluate_out(Y, Y1)) → MULT_IN(X1, Y1, Z)
MULT_IN(s(X), Y, R) → U151(X, Y, R, mult_in(X, Y, Z))
MULT_IN(s(X), Y, R) → MULT_IN(X, Y, Z)
U151(X, Y, R, mult_out(X, Y, Z)) → U161(X, Y, R, add_in(Y, Z, R))
U151(X, Y, R, mult_out(X, Y, Z)) → ADD_IN(Y, Z, R)

The TRS R consists of the following rules:

myis_in(Z, X) → U1(Z, X, evaluate_in(X, Z))
evaluate_in(X, X) → U11(X, myinteger_in(X))
myinteger_in(0) → myinteger_out(0)
myinteger_in(s(X)) → U12(X, myinteger_in(X))
U12(X, myinteger_out(X)) → myinteger_out(s(X))
U11(X, myinteger_out(X)) → evaluate_out(X, X)
evaluate_in(*(X, Y), Z) → U8(X, Y, Z, evaluate_in(X, X1))
evaluate_in(-(X, Y), Z) → U5(X, Y, Z, evaluate_in(X, X1))
evaluate_in(+(X, Y), Z) → U2(X, Y, Z, evaluate_in(X, X1))
U2(X, Y, Z, evaluate_out(X, X1)) → U3(X, Y, Z, X1, evaluate_in(Y, Y1))
U3(X, Y, Z, X1, evaluate_out(Y, Y1)) → U4(X, Y, Z, add_in(X1, Y1, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U4(X, Y, Z, add_out(X1, Y1, Z)) → evaluate_out(+(X, Y), Z)
U5(X, Y, Z, evaluate_out(X, X1)) → U6(X, Y, Z, X1, evaluate_in(Y, Y1))
U6(X, Y, Z, X1, evaluate_out(Y, Y1)) → U7(X, Y, Z, sub_in(X1, Y1, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U14(X, Y, Z, sub_in(X, Y, Z))
U14(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U7(X, Y, Z, sub_out(X1, Y1, Z)) → evaluate_out(-(X, Y), Z)
U8(X, Y, Z, evaluate_out(X, X1)) → U9(X, Y, Z, X1, evaluate_in(Y, Y1))
U9(X, Y, Z, X1, evaluate_out(Y, Y1)) → U10(X, Y, Z, mult_in(X1, Y1, Z))
mult_in(0, Y, 0) → mult_out(0, Y, 0)
mult_in(s(X), Y, R) → U15(X, Y, R, mult_in(X, Y, Z))
U15(X, Y, R, mult_out(X, Y, Z)) → U16(X, Y, R, add_in(Y, Z, R))
U16(X, Y, R, add_out(Y, Z, R)) → mult_out(s(X), Y, R)
U10(X, Y, Z, mult_out(X1, Y1, Z)) → evaluate_out(*(X, Y), Z)
U1(Z, X, evaluate_out(X, Z)) → myis_out(Z, X)

The argument filtering Pi contains the following mapping:
myis_in(x1, x2)  =  myis_in(x2)
U1(x1, x2, x3)  =  U1(x3)
evaluate_in(x1, x2)  =  evaluate_in(x1)
U11(x1, x2)  =  U11(x1, x2)
myinteger_in(x1)  =  myinteger_in(x1)
0  =  0
myinteger_out(x1)  =  myinteger_out
s(x1)  =  s(x1)
U12(x1, x2)  =  U12(x2)
evaluate_out(x1, x2)  =  evaluate_out(x2)
*(x1, x2)  =  *(x1, x2)
U8(x1, x2, x3, x4)  =  U8(x2, x4)
-(x1, x2)  =  -(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x4)
+(x1, x2)  =  +(x1, x2)
U2(x1, x2, x3, x4)  =  U2(x2, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x4, x5)
U4(x1, x2, x3, x4)  =  U4(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U13(x1, x2, x3, x4)  =  U13(x4)
U6(x1, x2, x3, x4, x5)  =  U6(x4, x5)
U7(x1, x2, x3, x4)  =  U7(x4)
sub_in(x1, x2, x3)  =  sub_in(x1, x2)
sub_out(x1, x2, x3)  =  sub_out(x3)
U14(x1, x2, x3, x4)  =  U14(x4)
U9(x1, x2, x3, x4, x5)  =  U9(x4, x5)
U10(x1, x2, x3, x4)  =  U10(x4)
mult_in(x1, x2, x3)  =  mult_in(x1, x2)
mult_out(x1, x2, x3)  =  mult_out(x3)
U15(x1, x2, x3, x4)  =  U15(x2, x4)
U16(x1, x2, x3, x4)  =  U16(x4)
myis_out(x1, x2)  =  myis_out(x1)
U151(x1, x2, x3, x4)  =  U151(x2, x4)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)
U101(x1, x2, x3, x4)  =  U101(x4)
U141(x1, x2, x3, x4)  =  U141(x4)
U41(x1, x2, x3, x4)  =  U41(x4)
MYINTEGER_IN(x1)  =  MYINTEGER_IN(x1)
U31(x1, x2, x3, x4, x5)  =  U31(x4, x5)
U121(x1, x2)  =  U121(x2)
U91(x1, x2, x3, x4, x5)  =  U91(x4, x5)
U21(x1, x2, x3, x4)  =  U21(x2, x4)
U61(x1, x2, x3, x4, x5)  =  U61(x4, x5)
U71(x1, x2, x3, x4)  =  U71(x4)
EVALUATE_IN(x1, x2)  =  EVALUATE_IN(x1)
U11(x1, x2, x3)  =  U11(x3)
U161(x1, x2, x3, x4)  =  U161(x4)
U111(x1, x2)  =  U111(x1, x2)
U51(x1, x2, x3, x4)  =  U51(x2, x4)
U131(x1, x2, x3, x4)  =  U131(x4)
SUB_IN(x1, x2, x3)  =  SUB_IN(x1, x2)
MYIS_IN(x1, x2)  =  MYIS_IN(x2)
U81(x1, x2, x3, x4)  =  U81(x2, x4)
MULT_IN(x1, x2, x3)  =  MULT_IN(x1, x2)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

MYIS_IN(Z, X) → U11(Z, X, evaluate_in(X, Z))
MYIS_IN(Z, X) → EVALUATE_IN(X, Z)
EVALUATE_IN(X, X) → U111(X, myinteger_in(X))
EVALUATE_IN(X, X) → MYINTEGER_IN(X)
MYINTEGER_IN(s(X)) → U121(X, myinteger_in(X))
MYINTEGER_IN(s(X)) → MYINTEGER_IN(X)
EVALUATE_IN(*(X, Y), Z) → U81(X, Y, Z, evaluate_in(X, X1))
EVALUATE_IN(*(X, Y), Z) → EVALUATE_IN(X, X1)
EVALUATE_IN(-(X, Y), Z) → U51(X, Y, Z, evaluate_in(X, X1))
EVALUATE_IN(-(X, Y), Z) → EVALUATE_IN(X, X1)
EVALUATE_IN(+(X, Y), Z) → U21(X, Y, Z, evaluate_in(X, X1))
EVALUATE_IN(+(X, Y), Z) → EVALUATE_IN(X, X1)
U21(X, Y, Z, evaluate_out(X, X1)) → U31(X, Y, Z, X1, evaluate_in(Y, Y1))
U21(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
U31(X, Y, Z, X1, evaluate_out(Y, Y1)) → U41(X, Y, Z, add_in(X1, Y1, Z))
U31(X, Y, Z, X1, evaluate_out(Y, Y1)) → ADD_IN(X1, Y1, Z)
ADD_IN(s(X), Y, s(Z)) → U131(X, Y, Z, add_in(X, Y, Z))
ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)
U51(X, Y, Z, evaluate_out(X, X1)) → U61(X, Y, Z, X1, evaluate_in(Y, Y1))
U51(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
U61(X, Y, Z, X1, evaluate_out(Y, Y1)) → U71(X, Y, Z, sub_in(X1, Y1, Z))
U61(X, Y, Z, X1, evaluate_out(Y, Y1)) → SUB_IN(X1, Y1, Z)
SUB_IN(s(X), s(Y), Z) → U141(X, Y, Z, sub_in(X, Y, Z))
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
U81(X, Y, Z, evaluate_out(X, X1)) → U91(X, Y, Z, X1, evaluate_in(Y, Y1))
U81(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
U91(X, Y, Z, X1, evaluate_out(Y, Y1)) → U101(X, Y, Z, mult_in(X1, Y1, Z))
U91(X, Y, Z, X1, evaluate_out(Y, Y1)) → MULT_IN(X1, Y1, Z)
MULT_IN(s(X), Y, R) → U151(X, Y, R, mult_in(X, Y, Z))
MULT_IN(s(X), Y, R) → MULT_IN(X, Y, Z)
U151(X, Y, R, mult_out(X, Y, Z)) → U161(X, Y, R, add_in(Y, Z, R))
U151(X, Y, R, mult_out(X, Y, Z)) → ADD_IN(Y, Z, R)

The TRS R consists of the following rules:

myis_in(Z, X) → U1(Z, X, evaluate_in(X, Z))
evaluate_in(X, X) → U11(X, myinteger_in(X))
myinteger_in(0) → myinteger_out(0)
myinteger_in(s(X)) → U12(X, myinteger_in(X))
U12(X, myinteger_out(X)) → myinteger_out(s(X))
U11(X, myinteger_out(X)) → evaluate_out(X, X)
evaluate_in(*(X, Y), Z) → U8(X, Y, Z, evaluate_in(X, X1))
evaluate_in(-(X, Y), Z) → U5(X, Y, Z, evaluate_in(X, X1))
evaluate_in(+(X, Y), Z) → U2(X, Y, Z, evaluate_in(X, X1))
U2(X, Y, Z, evaluate_out(X, X1)) → U3(X, Y, Z, X1, evaluate_in(Y, Y1))
U3(X, Y, Z, X1, evaluate_out(Y, Y1)) → U4(X, Y, Z, add_in(X1, Y1, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U4(X, Y, Z, add_out(X1, Y1, Z)) → evaluate_out(+(X, Y), Z)
U5(X, Y, Z, evaluate_out(X, X1)) → U6(X, Y, Z, X1, evaluate_in(Y, Y1))
U6(X, Y, Z, X1, evaluate_out(Y, Y1)) → U7(X, Y, Z, sub_in(X1, Y1, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U14(X, Y, Z, sub_in(X, Y, Z))
U14(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U7(X, Y, Z, sub_out(X1, Y1, Z)) → evaluate_out(-(X, Y), Z)
U8(X, Y, Z, evaluate_out(X, X1)) → U9(X, Y, Z, X1, evaluate_in(Y, Y1))
U9(X, Y, Z, X1, evaluate_out(Y, Y1)) → U10(X, Y, Z, mult_in(X1, Y1, Z))
mult_in(0, Y, 0) → mult_out(0, Y, 0)
mult_in(s(X), Y, R) → U15(X, Y, R, mult_in(X, Y, Z))
U15(X, Y, R, mult_out(X, Y, Z)) → U16(X, Y, R, add_in(Y, Z, R))
U16(X, Y, R, add_out(Y, Z, R)) → mult_out(s(X), Y, R)
U10(X, Y, Z, mult_out(X1, Y1, Z)) → evaluate_out(*(X, Y), Z)
U1(Z, X, evaluate_out(X, Z)) → myis_out(Z, X)

The argument filtering Pi contains the following mapping:
myis_in(x1, x2)  =  myis_in(x2)
U1(x1, x2, x3)  =  U1(x3)
evaluate_in(x1, x2)  =  evaluate_in(x1)
U11(x1, x2)  =  U11(x1, x2)
myinteger_in(x1)  =  myinteger_in(x1)
0  =  0
myinteger_out(x1)  =  myinteger_out
s(x1)  =  s(x1)
U12(x1, x2)  =  U12(x2)
evaluate_out(x1, x2)  =  evaluate_out(x2)
*(x1, x2)  =  *(x1, x2)
U8(x1, x2, x3, x4)  =  U8(x2, x4)
-(x1, x2)  =  -(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x4)
+(x1, x2)  =  +(x1, x2)
U2(x1, x2, x3, x4)  =  U2(x2, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x4, x5)
U4(x1, x2, x3, x4)  =  U4(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U13(x1, x2, x3, x4)  =  U13(x4)
U6(x1, x2, x3, x4, x5)  =  U6(x4, x5)
U7(x1, x2, x3, x4)  =  U7(x4)
sub_in(x1, x2, x3)  =  sub_in(x1, x2)
sub_out(x1, x2, x3)  =  sub_out(x3)
U14(x1, x2, x3, x4)  =  U14(x4)
U9(x1, x2, x3, x4, x5)  =  U9(x4, x5)
U10(x1, x2, x3, x4)  =  U10(x4)
mult_in(x1, x2, x3)  =  mult_in(x1, x2)
mult_out(x1, x2, x3)  =  mult_out(x3)
U15(x1, x2, x3, x4)  =  U15(x2, x4)
U16(x1, x2, x3, x4)  =  U16(x4)
myis_out(x1, x2)  =  myis_out(x1)
U151(x1, x2, x3, x4)  =  U151(x2, x4)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)
U101(x1, x2, x3, x4)  =  U101(x4)
U141(x1, x2, x3, x4)  =  U141(x4)
U41(x1, x2, x3, x4)  =  U41(x4)
MYINTEGER_IN(x1)  =  MYINTEGER_IN(x1)
U31(x1, x2, x3, x4, x5)  =  U31(x4, x5)
U121(x1, x2)  =  U121(x2)
U91(x1, x2, x3, x4, x5)  =  U91(x4, x5)
U21(x1, x2, x3, x4)  =  U21(x2, x4)
U61(x1, x2, x3, x4, x5)  =  U61(x4, x5)
U71(x1, x2, x3, x4)  =  U71(x4)
EVALUATE_IN(x1, x2)  =  EVALUATE_IN(x1)
U11(x1, x2, x3)  =  U11(x3)
U161(x1, x2, x3, x4)  =  U161(x4)
U111(x1, x2)  =  U111(x1, x2)
U51(x1, x2, x3, x4)  =  U51(x2, x4)
U131(x1, x2, x3, x4)  =  U131(x4)
SUB_IN(x1, x2, x3)  =  SUB_IN(x1, x2)
MYIS_IN(x1, x2)  =  MYIS_IN(x2)
U81(x1, x2, x3, x4)  =  U81(x2, x4)
MULT_IN(x1, x2, x3)  =  MULT_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 5 SCCs with 19 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)

The TRS R consists of the following rules:

myis_in(Z, X) → U1(Z, X, evaluate_in(X, Z))
evaluate_in(X, X) → U11(X, myinteger_in(X))
myinteger_in(0) → myinteger_out(0)
myinteger_in(s(X)) → U12(X, myinteger_in(X))
U12(X, myinteger_out(X)) → myinteger_out(s(X))
U11(X, myinteger_out(X)) → evaluate_out(X, X)
evaluate_in(*(X, Y), Z) → U8(X, Y, Z, evaluate_in(X, X1))
evaluate_in(-(X, Y), Z) → U5(X, Y, Z, evaluate_in(X, X1))
evaluate_in(+(X, Y), Z) → U2(X, Y, Z, evaluate_in(X, X1))
U2(X, Y, Z, evaluate_out(X, X1)) → U3(X, Y, Z, X1, evaluate_in(Y, Y1))
U3(X, Y, Z, X1, evaluate_out(Y, Y1)) → U4(X, Y, Z, add_in(X1, Y1, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U4(X, Y, Z, add_out(X1, Y1, Z)) → evaluate_out(+(X, Y), Z)
U5(X, Y, Z, evaluate_out(X, X1)) → U6(X, Y, Z, X1, evaluate_in(Y, Y1))
U6(X, Y, Z, X1, evaluate_out(Y, Y1)) → U7(X, Y, Z, sub_in(X1, Y1, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U14(X, Y, Z, sub_in(X, Y, Z))
U14(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U7(X, Y, Z, sub_out(X1, Y1, Z)) → evaluate_out(-(X, Y), Z)
U8(X, Y, Z, evaluate_out(X, X1)) → U9(X, Y, Z, X1, evaluate_in(Y, Y1))
U9(X, Y, Z, X1, evaluate_out(Y, Y1)) → U10(X, Y, Z, mult_in(X1, Y1, Z))
mult_in(0, Y, 0) → mult_out(0, Y, 0)
mult_in(s(X), Y, R) → U15(X, Y, R, mult_in(X, Y, Z))
U15(X, Y, R, mult_out(X, Y, Z)) → U16(X, Y, R, add_in(Y, Z, R))
U16(X, Y, R, add_out(Y, Z, R)) → mult_out(s(X), Y, R)
U10(X, Y, Z, mult_out(X1, Y1, Z)) → evaluate_out(*(X, Y), Z)
U1(Z, X, evaluate_out(X, Z)) → myis_out(Z, X)

The argument filtering Pi contains the following mapping:
myis_in(x1, x2)  =  myis_in(x2)
U1(x1, x2, x3)  =  U1(x3)
evaluate_in(x1, x2)  =  evaluate_in(x1)
U11(x1, x2)  =  U11(x1, x2)
myinteger_in(x1)  =  myinteger_in(x1)
0  =  0
myinteger_out(x1)  =  myinteger_out
s(x1)  =  s(x1)
U12(x1, x2)  =  U12(x2)
evaluate_out(x1, x2)  =  evaluate_out(x2)
*(x1, x2)  =  *(x1, x2)
U8(x1, x2, x3, x4)  =  U8(x2, x4)
-(x1, x2)  =  -(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x4)
+(x1, x2)  =  +(x1, x2)
U2(x1, x2, x3, x4)  =  U2(x2, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x4, x5)
U4(x1, x2, x3, x4)  =  U4(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U13(x1, x2, x3, x4)  =  U13(x4)
U6(x1, x2, x3, x4, x5)  =  U6(x4, x5)
U7(x1, x2, x3, x4)  =  U7(x4)
sub_in(x1, x2, x3)  =  sub_in(x1, x2)
sub_out(x1, x2, x3)  =  sub_out(x3)
U14(x1, x2, x3, x4)  =  U14(x4)
U9(x1, x2, x3, x4, x5)  =  U9(x4, x5)
U10(x1, x2, x3, x4)  =  U10(x4)
mult_in(x1, x2, x3)  =  mult_in(x1, x2)
mult_out(x1, x2, x3)  =  mult_out(x3)
U15(x1, x2, x3, x4)  =  U15(x2, x4)
U16(x1, x2, x3, x4)  =  U16(x4)
myis_out(x1, x2)  =  myis_out(x1)
SUB_IN(x1, x2, x3)  =  SUB_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUB_IN(x1, x2, x3)  =  SUB_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SUB_IN(s(X), s(Y)) → SUB_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)

The TRS R consists of the following rules:

myis_in(Z, X) → U1(Z, X, evaluate_in(X, Z))
evaluate_in(X, X) → U11(X, myinteger_in(X))
myinteger_in(0) → myinteger_out(0)
myinteger_in(s(X)) → U12(X, myinteger_in(X))
U12(X, myinteger_out(X)) → myinteger_out(s(X))
U11(X, myinteger_out(X)) → evaluate_out(X, X)
evaluate_in(*(X, Y), Z) → U8(X, Y, Z, evaluate_in(X, X1))
evaluate_in(-(X, Y), Z) → U5(X, Y, Z, evaluate_in(X, X1))
evaluate_in(+(X, Y), Z) → U2(X, Y, Z, evaluate_in(X, X1))
U2(X, Y, Z, evaluate_out(X, X1)) → U3(X, Y, Z, X1, evaluate_in(Y, Y1))
U3(X, Y, Z, X1, evaluate_out(Y, Y1)) → U4(X, Y, Z, add_in(X1, Y1, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U4(X, Y, Z, add_out(X1, Y1, Z)) → evaluate_out(+(X, Y), Z)
U5(X, Y, Z, evaluate_out(X, X1)) → U6(X, Y, Z, X1, evaluate_in(Y, Y1))
U6(X, Y, Z, X1, evaluate_out(Y, Y1)) → U7(X, Y, Z, sub_in(X1, Y1, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U14(X, Y, Z, sub_in(X, Y, Z))
U14(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U7(X, Y, Z, sub_out(X1, Y1, Z)) → evaluate_out(-(X, Y), Z)
U8(X, Y, Z, evaluate_out(X, X1)) → U9(X, Y, Z, X1, evaluate_in(Y, Y1))
U9(X, Y, Z, X1, evaluate_out(Y, Y1)) → U10(X, Y, Z, mult_in(X1, Y1, Z))
mult_in(0, Y, 0) → mult_out(0, Y, 0)
mult_in(s(X), Y, R) → U15(X, Y, R, mult_in(X, Y, Z))
U15(X, Y, R, mult_out(X, Y, Z)) → U16(X, Y, R, add_in(Y, Z, R))
U16(X, Y, R, add_out(Y, Z, R)) → mult_out(s(X), Y, R)
U10(X, Y, Z, mult_out(X1, Y1, Z)) → evaluate_out(*(X, Y), Z)
U1(Z, X, evaluate_out(X, Z)) → myis_out(Z, X)

The argument filtering Pi contains the following mapping:
myis_in(x1, x2)  =  myis_in(x2)
U1(x1, x2, x3)  =  U1(x3)
evaluate_in(x1, x2)  =  evaluate_in(x1)
U11(x1, x2)  =  U11(x1, x2)
myinteger_in(x1)  =  myinteger_in(x1)
0  =  0
myinteger_out(x1)  =  myinteger_out
s(x1)  =  s(x1)
U12(x1, x2)  =  U12(x2)
evaluate_out(x1, x2)  =  evaluate_out(x2)
*(x1, x2)  =  *(x1, x2)
U8(x1, x2, x3, x4)  =  U8(x2, x4)
-(x1, x2)  =  -(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x4)
+(x1, x2)  =  +(x1, x2)
U2(x1, x2, x3, x4)  =  U2(x2, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x4, x5)
U4(x1, x2, x3, x4)  =  U4(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U13(x1, x2, x3, x4)  =  U13(x4)
U6(x1, x2, x3, x4, x5)  =  U6(x4, x5)
U7(x1, x2, x3, x4)  =  U7(x4)
sub_in(x1, x2, x3)  =  sub_in(x1, x2)
sub_out(x1, x2, x3)  =  sub_out(x3)
U14(x1, x2, x3, x4)  =  U14(x4)
U9(x1, x2, x3, x4, x5)  =  U9(x4, x5)
U10(x1, x2, x3, x4)  =  U10(x4)
mult_in(x1, x2, x3)  =  mult_in(x1, x2)
mult_out(x1, x2, x3)  =  mult_out(x3)
U15(x1, x2, x3, x4)  =  U15(x2, x4)
U16(x1, x2, x3, x4)  =  U16(x4)
myis_out(x1, x2)  =  myis_out(x1)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ADD_IN(s(X), Y) → ADD_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MULT_IN(s(X), Y, R) → MULT_IN(X, Y, Z)

The TRS R consists of the following rules:

myis_in(Z, X) → U1(Z, X, evaluate_in(X, Z))
evaluate_in(X, X) → U11(X, myinteger_in(X))
myinteger_in(0) → myinteger_out(0)
myinteger_in(s(X)) → U12(X, myinteger_in(X))
U12(X, myinteger_out(X)) → myinteger_out(s(X))
U11(X, myinteger_out(X)) → evaluate_out(X, X)
evaluate_in(*(X, Y), Z) → U8(X, Y, Z, evaluate_in(X, X1))
evaluate_in(-(X, Y), Z) → U5(X, Y, Z, evaluate_in(X, X1))
evaluate_in(+(X, Y), Z) → U2(X, Y, Z, evaluate_in(X, X1))
U2(X, Y, Z, evaluate_out(X, X1)) → U3(X, Y, Z, X1, evaluate_in(Y, Y1))
U3(X, Y, Z, X1, evaluate_out(Y, Y1)) → U4(X, Y, Z, add_in(X1, Y1, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U4(X, Y, Z, add_out(X1, Y1, Z)) → evaluate_out(+(X, Y), Z)
U5(X, Y, Z, evaluate_out(X, X1)) → U6(X, Y, Z, X1, evaluate_in(Y, Y1))
U6(X, Y, Z, X1, evaluate_out(Y, Y1)) → U7(X, Y, Z, sub_in(X1, Y1, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U14(X, Y, Z, sub_in(X, Y, Z))
U14(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U7(X, Y, Z, sub_out(X1, Y1, Z)) → evaluate_out(-(X, Y), Z)
U8(X, Y, Z, evaluate_out(X, X1)) → U9(X, Y, Z, X1, evaluate_in(Y, Y1))
U9(X, Y, Z, X1, evaluate_out(Y, Y1)) → U10(X, Y, Z, mult_in(X1, Y1, Z))
mult_in(0, Y, 0) → mult_out(0, Y, 0)
mult_in(s(X), Y, R) → U15(X, Y, R, mult_in(X, Y, Z))
U15(X, Y, R, mult_out(X, Y, Z)) → U16(X, Y, R, add_in(Y, Z, R))
U16(X, Y, R, add_out(Y, Z, R)) → mult_out(s(X), Y, R)
U10(X, Y, Z, mult_out(X1, Y1, Z)) → evaluate_out(*(X, Y), Z)
U1(Z, X, evaluate_out(X, Z)) → myis_out(Z, X)

The argument filtering Pi contains the following mapping:
myis_in(x1, x2)  =  myis_in(x2)
U1(x1, x2, x3)  =  U1(x3)
evaluate_in(x1, x2)  =  evaluate_in(x1)
U11(x1, x2)  =  U11(x1, x2)
myinteger_in(x1)  =  myinteger_in(x1)
0  =  0
myinteger_out(x1)  =  myinteger_out
s(x1)  =  s(x1)
U12(x1, x2)  =  U12(x2)
evaluate_out(x1, x2)  =  evaluate_out(x2)
*(x1, x2)  =  *(x1, x2)
U8(x1, x2, x3, x4)  =  U8(x2, x4)
-(x1, x2)  =  -(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x4)
+(x1, x2)  =  +(x1, x2)
U2(x1, x2, x3, x4)  =  U2(x2, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x4, x5)
U4(x1, x2, x3, x4)  =  U4(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U13(x1, x2, x3, x4)  =  U13(x4)
U6(x1, x2, x3, x4, x5)  =  U6(x4, x5)
U7(x1, x2, x3, x4)  =  U7(x4)
sub_in(x1, x2, x3)  =  sub_in(x1, x2)
sub_out(x1, x2, x3)  =  sub_out(x3)
U14(x1, x2, x3, x4)  =  U14(x4)
U9(x1, x2, x3, x4, x5)  =  U9(x4, x5)
U10(x1, x2, x3, x4)  =  U10(x4)
mult_in(x1, x2, x3)  =  mult_in(x1, x2)
mult_out(x1, x2, x3)  =  mult_out(x3)
U15(x1, x2, x3, x4)  =  U15(x2, x4)
U16(x1, x2, x3, x4)  =  U16(x4)
myis_out(x1, x2)  =  myis_out(x1)
MULT_IN(x1, x2, x3)  =  MULT_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MULT_IN(s(X), Y, R) → MULT_IN(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULT_IN(x1, x2, x3)  =  MULT_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MULT_IN(s(X), Y) → MULT_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MYINTEGER_IN(s(X)) → MYINTEGER_IN(X)

The TRS R consists of the following rules:

myis_in(Z, X) → U1(Z, X, evaluate_in(X, Z))
evaluate_in(X, X) → U11(X, myinteger_in(X))
myinteger_in(0) → myinteger_out(0)
myinteger_in(s(X)) → U12(X, myinteger_in(X))
U12(X, myinteger_out(X)) → myinteger_out(s(X))
U11(X, myinteger_out(X)) → evaluate_out(X, X)
evaluate_in(*(X, Y), Z) → U8(X, Y, Z, evaluate_in(X, X1))
evaluate_in(-(X, Y), Z) → U5(X, Y, Z, evaluate_in(X, X1))
evaluate_in(+(X, Y), Z) → U2(X, Y, Z, evaluate_in(X, X1))
U2(X, Y, Z, evaluate_out(X, X1)) → U3(X, Y, Z, X1, evaluate_in(Y, Y1))
U3(X, Y, Z, X1, evaluate_out(Y, Y1)) → U4(X, Y, Z, add_in(X1, Y1, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U4(X, Y, Z, add_out(X1, Y1, Z)) → evaluate_out(+(X, Y), Z)
U5(X, Y, Z, evaluate_out(X, X1)) → U6(X, Y, Z, X1, evaluate_in(Y, Y1))
U6(X, Y, Z, X1, evaluate_out(Y, Y1)) → U7(X, Y, Z, sub_in(X1, Y1, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U14(X, Y, Z, sub_in(X, Y, Z))
U14(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U7(X, Y, Z, sub_out(X1, Y1, Z)) → evaluate_out(-(X, Y), Z)
U8(X, Y, Z, evaluate_out(X, X1)) → U9(X, Y, Z, X1, evaluate_in(Y, Y1))
U9(X, Y, Z, X1, evaluate_out(Y, Y1)) → U10(X, Y, Z, mult_in(X1, Y1, Z))
mult_in(0, Y, 0) → mult_out(0, Y, 0)
mult_in(s(X), Y, R) → U15(X, Y, R, mult_in(X, Y, Z))
U15(X, Y, R, mult_out(X, Y, Z)) → U16(X, Y, R, add_in(Y, Z, R))
U16(X, Y, R, add_out(Y, Z, R)) → mult_out(s(X), Y, R)
U10(X, Y, Z, mult_out(X1, Y1, Z)) → evaluate_out(*(X, Y), Z)
U1(Z, X, evaluate_out(X, Z)) → myis_out(Z, X)

The argument filtering Pi contains the following mapping:
myis_in(x1, x2)  =  myis_in(x2)
U1(x1, x2, x3)  =  U1(x3)
evaluate_in(x1, x2)  =  evaluate_in(x1)
U11(x1, x2)  =  U11(x1, x2)
myinteger_in(x1)  =  myinteger_in(x1)
0  =  0
myinteger_out(x1)  =  myinteger_out
s(x1)  =  s(x1)
U12(x1, x2)  =  U12(x2)
evaluate_out(x1, x2)  =  evaluate_out(x2)
*(x1, x2)  =  *(x1, x2)
U8(x1, x2, x3, x4)  =  U8(x2, x4)
-(x1, x2)  =  -(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x4)
+(x1, x2)  =  +(x1, x2)
U2(x1, x2, x3, x4)  =  U2(x2, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x4, x5)
U4(x1, x2, x3, x4)  =  U4(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U13(x1, x2, x3, x4)  =  U13(x4)
U6(x1, x2, x3, x4, x5)  =  U6(x4, x5)
U7(x1, x2, x3, x4)  =  U7(x4)
sub_in(x1, x2, x3)  =  sub_in(x1, x2)
sub_out(x1, x2, x3)  =  sub_out(x3)
U14(x1, x2, x3, x4)  =  U14(x4)
U9(x1, x2, x3, x4, x5)  =  U9(x4, x5)
U10(x1, x2, x3, x4)  =  U10(x4)
mult_in(x1, x2, x3)  =  mult_in(x1, x2)
mult_out(x1, x2, x3)  =  mult_out(x3)
U15(x1, x2, x3, x4)  =  U15(x2, x4)
U16(x1, x2, x3, x4)  =  U16(x4)
myis_out(x1, x2)  =  myis_out(x1)
MYINTEGER_IN(x1)  =  MYINTEGER_IN(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MYINTEGER_IN(s(X)) → MYINTEGER_IN(X)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MYINTEGER_IN(s(X)) → MYINTEGER_IN(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

U21(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
EVALUATE_IN(*(X, Y), Z) → U81(X, Y, Z, evaluate_in(X, X1))
EVALUATE_IN(-(X, Y), Z) → EVALUATE_IN(X, X1)
U51(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
EVALUATE_IN(-(X, Y), Z) → U51(X, Y, Z, evaluate_in(X, X1))
U81(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
EVALUATE_IN(+(X, Y), Z) → U21(X, Y, Z, evaluate_in(X, X1))
EVALUATE_IN(+(X, Y), Z) → EVALUATE_IN(X, X1)
EVALUATE_IN(*(X, Y), Z) → EVALUATE_IN(X, X1)

The TRS R consists of the following rules:

myis_in(Z, X) → U1(Z, X, evaluate_in(X, Z))
evaluate_in(X, X) → U11(X, myinteger_in(X))
myinteger_in(0) → myinteger_out(0)
myinteger_in(s(X)) → U12(X, myinteger_in(X))
U12(X, myinteger_out(X)) → myinteger_out(s(X))
U11(X, myinteger_out(X)) → evaluate_out(X, X)
evaluate_in(*(X, Y), Z) → U8(X, Y, Z, evaluate_in(X, X1))
evaluate_in(-(X, Y), Z) → U5(X, Y, Z, evaluate_in(X, X1))
evaluate_in(+(X, Y), Z) → U2(X, Y, Z, evaluate_in(X, X1))
U2(X, Y, Z, evaluate_out(X, X1)) → U3(X, Y, Z, X1, evaluate_in(Y, Y1))
U3(X, Y, Z, X1, evaluate_out(Y, Y1)) → U4(X, Y, Z, add_in(X1, Y1, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U4(X, Y, Z, add_out(X1, Y1, Z)) → evaluate_out(+(X, Y), Z)
U5(X, Y, Z, evaluate_out(X, X1)) → U6(X, Y, Z, X1, evaluate_in(Y, Y1))
U6(X, Y, Z, X1, evaluate_out(Y, Y1)) → U7(X, Y, Z, sub_in(X1, Y1, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U14(X, Y, Z, sub_in(X, Y, Z))
U14(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U7(X, Y, Z, sub_out(X1, Y1, Z)) → evaluate_out(-(X, Y), Z)
U8(X, Y, Z, evaluate_out(X, X1)) → U9(X, Y, Z, X1, evaluate_in(Y, Y1))
U9(X, Y, Z, X1, evaluate_out(Y, Y1)) → U10(X, Y, Z, mult_in(X1, Y1, Z))
mult_in(0, Y, 0) → mult_out(0, Y, 0)
mult_in(s(X), Y, R) → U15(X, Y, R, mult_in(X, Y, Z))
U15(X, Y, R, mult_out(X, Y, Z)) → U16(X, Y, R, add_in(Y, Z, R))
U16(X, Y, R, add_out(Y, Z, R)) → mult_out(s(X), Y, R)
U10(X, Y, Z, mult_out(X1, Y1, Z)) → evaluate_out(*(X, Y), Z)
U1(Z, X, evaluate_out(X, Z)) → myis_out(Z, X)

The argument filtering Pi contains the following mapping:
myis_in(x1, x2)  =  myis_in(x2)
U1(x1, x2, x3)  =  U1(x3)
evaluate_in(x1, x2)  =  evaluate_in(x1)
U11(x1, x2)  =  U11(x1, x2)
myinteger_in(x1)  =  myinteger_in(x1)
0  =  0
myinteger_out(x1)  =  myinteger_out
s(x1)  =  s(x1)
U12(x1, x2)  =  U12(x2)
evaluate_out(x1, x2)  =  evaluate_out(x2)
*(x1, x2)  =  *(x1, x2)
U8(x1, x2, x3, x4)  =  U8(x2, x4)
-(x1, x2)  =  -(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x4)
+(x1, x2)  =  +(x1, x2)
U2(x1, x2, x3, x4)  =  U2(x2, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x4, x5)
U4(x1, x2, x3, x4)  =  U4(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U13(x1, x2, x3, x4)  =  U13(x4)
U6(x1, x2, x3, x4, x5)  =  U6(x4, x5)
U7(x1, x2, x3, x4)  =  U7(x4)
sub_in(x1, x2, x3)  =  sub_in(x1, x2)
sub_out(x1, x2, x3)  =  sub_out(x3)
U14(x1, x2, x3, x4)  =  U14(x4)
U9(x1, x2, x3, x4, x5)  =  U9(x4, x5)
U10(x1, x2, x3, x4)  =  U10(x4)
mult_in(x1, x2, x3)  =  mult_in(x1, x2)
mult_out(x1, x2, x3)  =  mult_out(x3)
U15(x1, x2, x3, x4)  =  U15(x2, x4)
U16(x1, x2, x3, x4)  =  U16(x4)
myis_out(x1, x2)  =  myis_out(x1)
U21(x1, x2, x3, x4)  =  U21(x2, x4)
EVALUATE_IN(x1, x2)  =  EVALUATE_IN(x1)
U51(x1, x2, x3, x4)  =  U51(x2, x4)
U81(x1, x2, x3, x4)  =  U81(x2, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U21(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
EVALUATE_IN(*(X, Y), Z) → U81(X, Y, Z, evaluate_in(X, X1))
EVALUATE_IN(-(X, Y), Z) → EVALUATE_IN(X, X1)
U51(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
EVALUATE_IN(-(X, Y), Z) → U51(X, Y, Z, evaluate_in(X, X1))
U81(X, Y, Z, evaluate_out(X, X1)) → EVALUATE_IN(Y, Y1)
EVALUATE_IN(+(X, Y), Z) → U21(X, Y, Z, evaluate_in(X, X1))
EVALUATE_IN(+(X, Y), Z) → EVALUATE_IN(X, X1)
EVALUATE_IN(*(X, Y), Z) → EVALUATE_IN(X, X1)

The TRS R consists of the following rules:

evaluate_in(X, X) → U11(X, myinteger_in(X))
evaluate_in(*(X, Y), Z) → U8(X, Y, Z, evaluate_in(X, X1))
evaluate_in(-(X, Y), Z) → U5(X, Y, Z, evaluate_in(X, X1))
evaluate_in(+(X, Y), Z) → U2(X, Y, Z, evaluate_in(X, X1))
U11(X, myinteger_out(X)) → evaluate_out(X, X)
U8(X, Y, Z, evaluate_out(X, X1)) → U9(X, Y, Z, X1, evaluate_in(Y, Y1))
U5(X, Y, Z, evaluate_out(X, X1)) → U6(X, Y, Z, X1, evaluate_in(Y, Y1))
U2(X, Y, Z, evaluate_out(X, X1)) → U3(X, Y, Z, X1, evaluate_in(Y, Y1))
myinteger_in(0) → myinteger_out(0)
myinteger_in(s(X)) → U12(X, myinteger_in(X))
U9(X, Y, Z, X1, evaluate_out(Y, Y1)) → U10(X, Y, Z, mult_in(X1, Y1, Z))
U6(X, Y, Z, X1, evaluate_out(Y, Y1)) → U7(X, Y, Z, sub_in(X1, Y1, Z))
U3(X, Y, Z, X1, evaluate_out(Y, Y1)) → U4(X, Y, Z, add_in(X1, Y1, Z))
U12(X, myinteger_out(X)) → myinteger_out(s(X))
U10(X, Y, Z, mult_out(X1, Y1, Z)) → evaluate_out(*(X, Y), Z)
U7(X, Y, Z, sub_out(X1, Y1, Z)) → evaluate_out(-(X, Y), Z)
U4(X, Y, Z, add_out(X1, Y1, Z)) → evaluate_out(+(X, Y), Z)
mult_in(0, Y, 0) → mult_out(0, Y, 0)
mult_in(s(X), Y, R) → U15(X, Y, R, mult_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U14(X, Y, Z, sub_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
U15(X, Y, R, mult_out(X, Y, Z)) → U16(X, Y, R, add_in(Y, Z, R))
U14(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U16(X, Y, R, add_out(Y, Z, R)) → mult_out(s(X), Y, R)

The argument filtering Pi contains the following mapping:
evaluate_in(x1, x2)  =  evaluate_in(x1)
U11(x1, x2)  =  U11(x1, x2)
myinteger_in(x1)  =  myinteger_in(x1)
0  =  0
myinteger_out(x1)  =  myinteger_out
s(x1)  =  s(x1)
U12(x1, x2)  =  U12(x2)
evaluate_out(x1, x2)  =  evaluate_out(x2)
*(x1, x2)  =  *(x1, x2)
U8(x1, x2, x3, x4)  =  U8(x2, x4)
-(x1, x2)  =  -(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x4)
+(x1, x2)  =  +(x1, x2)
U2(x1, x2, x3, x4)  =  U2(x2, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x4, x5)
U4(x1, x2, x3, x4)  =  U4(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
add_out(x1, x2, x3)  =  add_out(x3)
U13(x1, x2, x3, x4)  =  U13(x4)
U6(x1, x2, x3, x4, x5)  =  U6(x4, x5)
U7(x1, x2, x3, x4)  =  U7(x4)
sub_in(x1, x2, x3)  =  sub_in(x1, x2)
sub_out(x1, x2, x3)  =  sub_out(x3)
U14(x1, x2, x3, x4)  =  U14(x4)
U9(x1, x2, x3, x4, x5)  =  U9(x4, x5)
U10(x1, x2, x3, x4)  =  U10(x4)
mult_in(x1, x2, x3)  =  mult_in(x1, x2)
mult_out(x1, x2, x3)  =  mult_out(x3)
U15(x1, x2, x3, x4)  =  U15(x2, x4)
U16(x1, x2, x3, x4)  =  U16(x4)
U21(x1, x2, x3, x4)  =  U21(x2, x4)
EVALUATE_IN(x1, x2)  =  EVALUATE_IN(x1)
U51(x1, x2, x3, x4)  =  U51(x2, x4)
U81(x1, x2, x3, x4)  =  U81(x2, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

EVALUATE_IN(+(X, Y)) → U21(Y, evaluate_in(X))
EVALUATE_IN(*(X, Y)) → EVALUATE_IN(X)
EVALUATE_IN(-(X, Y)) → EVALUATE_IN(X)
EVALUATE_IN(-(X, Y)) → U51(Y, evaluate_in(X))
EVALUATE_IN(+(X, Y)) → EVALUATE_IN(X)
U51(Y, evaluate_out(X1)) → EVALUATE_IN(Y)
U21(Y, evaluate_out(X1)) → EVALUATE_IN(Y)
EVALUATE_IN(*(X, Y)) → U81(Y, evaluate_in(X))
U81(Y, evaluate_out(X1)) → EVALUATE_IN(Y)

The TRS R consists of the following rules:

evaluate_in(X) → U11(X, myinteger_in(X))
evaluate_in(*(X, Y)) → U8(Y, evaluate_in(X))
evaluate_in(-(X, Y)) → U5(Y, evaluate_in(X))
evaluate_in(+(X, Y)) → U2(Y, evaluate_in(X))
U11(X, myinteger_out) → evaluate_out(X)
U8(Y, evaluate_out(X1)) → U9(X1, evaluate_in(Y))
U5(Y, evaluate_out(X1)) → U6(X1, evaluate_in(Y))
U2(Y, evaluate_out(X1)) → U3(X1, evaluate_in(Y))
myinteger_in(0) → myinteger_out
myinteger_in(s(X)) → U12(myinteger_in(X))
U9(X1, evaluate_out(Y1)) → U10(mult_in(X1, Y1))
U6(X1, evaluate_out(Y1)) → U7(sub_in(X1, Y1))
U3(X1, evaluate_out(Y1)) → U4(add_in(X1, Y1))
U12(myinteger_out) → myinteger_out
U10(mult_out(Z)) → evaluate_out(Z)
U7(sub_out(Z)) → evaluate_out(Z)
U4(add_out(Z)) → evaluate_out(Z)
mult_in(0, Y) → mult_out(0)
mult_in(s(X), Y) → U15(Y, mult_in(X, Y))
sub_in(X, 0) → sub_out(X)
sub_in(s(X), s(Y)) → U14(sub_in(X, Y))
add_in(0, X) → add_out(X)
add_in(s(X), Y) → U13(add_in(X, Y))
U15(Y, mult_out(Z)) → U16(add_in(Y, Z))
U14(sub_out(Z)) → sub_out(Z)
U13(add_out(Z)) → add_out(s(Z))
U16(add_out(R)) → mult_out(R)

The set Q consists of the following terms:

evaluate_in(x0)
U11(x0, x1)
U8(x0, x1)
U5(x0, x1)
U2(x0, x1)
myinteger_in(x0)
U9(x0, x1)
U6(x0, x1)
U3(x0, x1)
U12(x0)
U10(x0)
U7(x0)
U4(x0)
mult_in(x0, x1)
sub_in(x0, x1)
add_in(x0, x1)
U15(x0, x1)
U14(x0)
U13(x0)
U16(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: